ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da). ecl-max(x)   

latex

Definitions	x. t(x), x,y,z. t(x;y;z), x,y,z,w. t(x;y;z;w), False, P  Q, A, A  B, x,y. t(x;y), ecl-max(x), , t  T, x:A. B(x), x(s), , x(s1,s2,s3), x(s1,s2,s3,s4), x(s1,s2)
Lemmas	Id wf, fpf wf, ecl wf, lt int wf, ifthenelse wf, Knd wf, bool wf, ma-valtype wf, decl-state wf, le wf, nat wf, ecl ind wf